The memory model of a shared-memory multiprocessor is a contract between thedesigner and programmer of the multiprocessor. The sequential consistencymemory model specifies a total order among the memory (read and write) eventsperformed at each processor. A trace of a memory system satisfies sequentialconsistency if there exists a total order of all memory events in the tracethat is both consistent with the total order at each processor and has theproperty that every read event to a location returns the value of the lastwrite to that location. Descriptions of shared-memory systems are typically parameterized by thenumber of processors, the number of memory locations, and the number of datavalues. It has been shown that even for finite parameter values, verifyingsequential consistency on general shared-memory systems is undecidable. Weobserve that, in practice, shared-memory systems satisfy the properties ofcausality and data independence. Causality is the property that values of readevents flow from values of write events. Data independence is the property thatall traces can be generated by renaming data values from traces where thewritten values are distinct from each other. If a causal and data independentsystem also has the property that the logical order of write events to eachlocation is identical to their temporal order, then sequential consistency canbe verified algorithmically. Specifically, we present a model checkingalgorithm to verify sequential consistency on such systems for a finite numberof processors and memory locations and an arbitrary number of data values.
展开▼
